Inference at * 1 0 1 1 1 
Iof proof for Lemma integer sqrt:



1. n : 
2. n < 0
3. ((n+1)  0 )  (r:. (((r * r)  (n+1)) & ((n+1) < ((r+1) * (r+1)))))
4. n  0 
  r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by Arith 

latex

 .

Definitions	x:A  B(x), x:AB(x), Void, a < b, , t  T, i  j , A  B, A, False, P  Q, x:A. B(x), P & Q
Lemmas	nat wf